Correspondencia Curry-Howard

CORRESPONDENCIA
CURRY-HOWARD

“Los tipos son proposiciones. Los programas son demostraciones” (Haskell Curry)

La Correspondencia Curry-Howard
La correspondencia (o isomorfismo) Curry-Howard −por sus proponentes, los lógicos Haskell Curry y William Alvin Howard− se considera uno de los grandes descubrimientos en lógica. Se basa en una idea sorprendentemente simple pero con profundas consecuencias en la relación entre lógica e informática:

A un tipo A de elementos le corresponde la proposición lógica A_p “A está habitado” o “A no está vacío”.
Un elemento de tipo A es una demostración de la proposición A_p, pues si el tipo A no es vacío, entonces la proposición A_p es verdadera.

Por ejemplo, si int es el tipo de los números enteros, la proposición asociada es int_p “los enteros están habitados”. Si 3 es un entero, entonces este número es la demostración de la proposición int_p. Si un lenguaje de programación tiene enteros, es decir, si tiene tipo int, entonces int_p es V (verdadera) y F (falsa) si no los tiene.

Una vez que tenemos proposiciones lógicas asociadas a tipos, es posible definir proposiciones compuestas (con operadores lógicos) basadas en tipos:

Implicación.
Si tenemos una función f con un argumento de tipo A y que produce como resultado un elemento de tipo B, entonces la función f es de tipo A→B, es decir, a cada elemento de tipo A le corresponde un elemento de tipo B.

A este tipo de función le corresponde la implicación A_p→B_p, en donde A_p es “A está habitado” y B_p es “B está habitado”. Esta implicación quiere decir que si A está habitado, entonces B está también habitado. Si A está habitado, hay un elemento a de tipo A y también hay un elemento de tipo B, que es f(a). Por lo tanto, B está habitado y B_p es V. En resumen, dado un elemento de tipo A, hay una demostración de A_p, y la función f construye un elemento de tipo B y una demostración de B_p.
Conjunción.
Si tenemos dos tipos, A y B, y las correspondientes proposiciones A_p y B_p, la conjunción de estas dos proposiciones es B_p∧A_p. Esta conjunción es V si A_p y B_p son ambas V. Para su demostración necesitamos una demostración de A_p y de B_p. Un elemento que incluye a ambas demostraciones es un par de elementos (a, b), en donde a es un elemento de tipo A, y b es un elemento de tipo B. El par (a, b) es un elemento del producto cartesiano C de los conjuntos formados por los elementos de tipo A y los de tipo B, respectivamente. Una demostración de la conjunción es, pues, un elemento de C.
Disyunción.
Si tenemos dos tipos, A y B, y las correspondientes proposiciones A_p y B_p, la disyunción de estas dos proposiciones es A_p∨B_p. Esta disyunción es V si A_p o B_p es V. Para su demostración necesitamos una demostración de A_p o de B_p. Un elemento que incluye a una de las dos demostraciones es un elemento que pertenece a la unión D de los conjuntos asociados a los tipos A y los de tipo B, respectivamente. Una demostración de la disyunción es un elemento de D.
Negación.
La negación de la proposición A_p “A está habitado” es A_p' “A no está habitado”.

Dada la correspondencia establecida entre tipos y proposiciones, se suele unificar la notación: un tipo A es equivalente a la proposición A. Por lo tanto:

A→B es a la vez un tipo y una proposición. Si A→B es un tipo habitado, la proposición A→B es un teorema.

Una implicación A→B se puede considerar un programa (o un tipo de función) donde A es el tipo de entrada y B el tipo de salida. La salida es la demostración de la implicación. Aplicación e implicación son duales entre sí.
Si A×B es un tipo habitado, la proposición A∧B es un teorema. La conjunción es un tipo de producto cartesiano.
Si A∪B es un tipo habitado, la proposición A∨B es un teorema. La disyunción es un tipo resultante de una unión de tipos.

Un programa que realice una demostración tiene unos tipos de entrada (que corresponden a proposiciones) y un tipo de salida (que corresponde a la proposición que se quiere demostrar).

Para demostrar un teorema lógico T, todo lo que tenemos que hacer es construir un tipo t basado en los tipos de entrada (que son axiomas) que refleje la estructura del teorema, y luego encontrar un elemento que tenga ese tipo t. Ejemplos de teoremas lógicos son

La correspondencia Curry-Howard inversa −por eso es un isomorfismo− es:

A cada proposición le corresponde un tipo. Si la proposición es verdadera, su tipo es V. Si la proposición es falsa, su tipo es F. Esto equivale a los conceptos de “sentido” y “referencia” fregeanos, en donde la proposición es el sentido y el valor de verdad su referencia.

La correspondencia Curry-Howard conecta:

Tipos con proposiciones. En general, tipos con fórmulas lógicas.
Lógica y lenguajes de programación con la lógica proposicional, dos áreas que antes no estaban relacionadas.
Lo estático (la lógica) con lo dinámico (la computación).
Demostraciones y programas. Se estandariza la forma de demostrar teoremas lógicos (proposiciones universalmente verdaderas) mediante programas. Los programas son demostraciones de teoremas lógicos. Las demostraciones, al representarse mediante programas, pueden automatizarse.

La correspondencia Curry-Howard y la unificación entre lógica e informática

Todo empezó en 1934, cuando Haskell Curry interpretó el tipo como proposición y un elemento del tipo como demostración de la proposición. En 1958, Curry llegó a la conclusión de que los tipos permitían expresar la lógica intuicionista.

Más tarde, William Alvin Howard descubrió que también se podían expresar gran número de lógicas intucionistas, incluyendo la lógica intuicionista de orden superior. En 1969, Howard descubrió una analogía formal entre los programas del cálculo lambda y las demostraciones de la deducción natural.

La deducción natural es una aproximación a la teoría de la demostración en la que se busca emular la manera en que las personas razonan al realizar demostraciones matemáticas. En lugar de utilizar diversos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone considerar el menor número posible de axiomas y ampliar el número de reglas de inferencia, introduciendo dos reglas para cada operador lógico (una para introducirla y otra para eliminarla). La deducción natural fue introducida por Gerhard Gentzen en su trabajo “Investigaciones sobre la inferencia lógica”, publicado en 1934-35. Desde el descubrimiento de la correspondencia Curry-Howard, la deducción natural ha cobrado una importancia significativa como fundamento de la informática (en especial para la programación funcional), pues su formulación se corresponde con el cálculo lambda. [ver Aplicaciones – Lógica – Deducción Natural.] La correspondencia Curry-Howard ha sido el motor de un gran espectro de nuevas investigaciones. En particular, ha conducido a una nueva clase de sistemas formales que pueden actuar como sistemas de demostración y como lenguajes de programación. Este campo de investigación se suele denominar “teoría de tipos moderna”. Se ha especulado incluso que la correspondencia Curry-Howard podría ser un elemento decisivo para lograr una fundamentación común de la lógica matemática y la informática.

Especificación en MENTAL
En primer lugar, hay que diferenciar entre clase y tipo:

Una clase es un conjunto de elementos que comparten una propiedad.
El tipo en informática es una propiedad intrínseca que tienen los elementos de una clase.

Una propiedad puede ser intrínseca (la que denota el propio elemento) o extrínseca (asociada desde fuera del elemento). Una propiedad extrínsca se denomina también atributo o predicado.

Si x es un elemento de una clase C y su tipo correspondiente es t, se cumple la propiedad:

⟨( x/t ↔ x∈C )⟩

x/t

x

t

x

t

x/t

x

t

Por ejemplo, si tenemos que D={0…9} es el conjunto de todos los dígitos, y llamamos d a su tipo correspondiente, se tiene la equivalencia condicional


(⟨ x/d ↔ x∈D )⟩

En la correspondencia Curry-Howard, si un elemento es de tipo t, eso implica la proposición t≠∅ (t está habitado o t no está vacío). En MENTAL, si un elemento x es de tipo t, se cumple x/t y ((x/t)? = α).

En MENTAL tenemos las siguientes características:

No se necesita interpretar el tipo como proposición, pues ambos son expresiones. Por consiguiente, la correspondencia Curry-Howard no es necesaria porque está implícita en el lenguaje.
Hay equivalencia entre tipo y predicado: si x tiene el predicado t, x es de tipo t. Por ejemplo,
- “Pepe es hombre” se representa como Pepe/hombre. Pepe tiene el predicado hombre y Pepe es un tipo de hombre.
- “3 es un entero” se representa como 3/entero. 3 es un tipo de entero y tiene el predicado entero.
- “3 es un dígito” se representa como 3/d. 3 es un tipo de d (dígito) y tiene el predicado d.
El tipo universal (o expresión universal) es α, que corresponde al predicado “existe” y que sustituye a la fórmula o proposición lógica V (verdadero). El tipo nulo (o expresión nula) es θ, que corresponde al predicado “no existe” y que sustituye a la fórmula lógica F (falso). Estos tipos universales de programación son los mismos que los tipos lógicos, es decir, se unifican los tipos lógicos y los tipos de programación. Son los mismos.
Las demostraciones son construcciones y no van ligadas al concepto dual V-F. No hay valores de verdad, sino valores existenciales (existencia y no-existencia), que son los auténticos valores lógicos que sirven para las decisiones y las implicaciones. La verdad se trata como magnitud cualitativa, de la forma f*V. La verdad es un predicado, por ejemplo, x/V o x/(0.7*V).
Los tipos se pueden combinar mediante las primitivas, como cualquier otra expresión, y por lo tanto puede haber tipos de orden superior, tipos parametrizados, tipos calculados, tipos entrelazados, tipos virtuales, etc. Tras los tipos está toda la potencia del lenguaje para crear nuevos tipos.
En la correspondencia Curry-Howard, los programas son demostraciones. En MENTAL, los programas son también demostraciones, que son construcciones realizadas mediante instancias de los axiomas semánticos.
Se cumple la propiedad
Es decir, si x es de tipo A e y es de tipo B, entonces x→y es de tipo A→B. Análogamente para la conjunción y la disyunción:

MENTAL y la unificación lógica - informática

Desde los tiempos de Gödel, Curry, Church, Turing, Shannon y von Neumann, los fundamentos de la informática han estado intrínsecamente ligados a la matemática, especialmente a la lógica matemática. Este vínculo histórico se vio reforzado con el descubrimiento de la correspondencia Curry-Howard, que proporcionó una conexión directa entre dos disciplinas: programación y lógica formal.

Sin embargo, este vínculo no se ha considerado suficiente, pues se deseaba lograr un isomorfismo completo entre programación y lógica clásica. Se intentaron tres principales alternativas. Unos autores partieron de la programación, seleccionando unas características particulares, como fundamento e intentaron adaptar la lógica clásica a un sistema de tipos. Otros autores eligieron el camino opuesto: eligieron la lógica como fundamento e intentaron derivar nuevos paradigmas, campos o conceptos de programación. Por último, un tercer grupo se centró en la búsqueda de un terreno común intermedio entre programación y lógica.

En esencia, los problemas eran dos: 1) cómo hacer computaciones con la lógica; 2) cómo hacer lógica con la computación.

MENTAL proporciona una respuesta muy sencilla a estos problemas. La respuesta consiste simplemente en trascender la lógica y la informática, de tal manera que la conexión entre informática y la lógica se realiza, no a nivel horizontal, sino a nivel vertical o profundo: mediante los arquetipos primarios:

La lógica se fundamenta en la primitiva “Condición”, que sirve para la lógica de decisión. Junto con una expresión genérica permite la lógica de la deducción o inferencia.
La primitiva “particularización” se utiliza para especificar tanto tipos como predicados. Un “tipo” es simplemente un tipo de predicado.
La lógica y la informática no se pueden unificar porque son disciplinas distintas, pero ambas tienen el mismo fundamento común: las primitivas semánticas universales, como lo tienen la lógica proposicional o la lógica de predicados.

De esta forma, no es necesario buscar un contenido computacional a la lógica clásica.

Bibliografía

Griffin, T.G. Formulae-as-types notion of control. In Conf. Record 17th annual ACM Symposium on Principles of Programming Languages, POPL’90, pp. 47–58. ACM Press, 1990.
Howard, William Alvin. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, 1980.
Krebbers, Robbert. Clasical logic, control calculi and data types. Master´s Thesis. October 2010. Internet.
Poernomo, Iman; Crossley, John N.; Wirsing, Martin. Adapting Proofs-as-Programs. The Curry--Howard Protocol. Springer, 2010.
Sheard, Tim. Putting Curry-Howard to Work. Internet.
Simmons, H. Derivation and Computation. Taking the Curry-Howard correspondence seriously. Cambridge University Press, 2000.
Sorensen, M.H. Lectures on the Curry-Howard Isomorphism. Elsevier Science, 2006.